feat(ProgramLogic): eRHL program logic, TV distance, Fiat-Shamir, and ElGamal IND-CPA by quangvdao · Pull Request #116 · Verified-zkEVM/VCV-io

quangvdao · 2026-03-04T23:08:45Z

Summary

Adds a game-hopping program logic framework (relational Hoare logic, TV distance infrastructure, oracle simulation rules) and applies it to prove ElGamal IND-CPA security reduces to DDH.

Program Logic (`VCVio/ProgramLogic/`)

Unary/SimulateQ: Oracle-aware weakest-precondition rules (wp_simulateQ_eq, wp_liftComp, wp_simulateQ_run'_eq) for reasoning through simulateQ boundaries.
Unary/HoareTriple: New wp_ite, wp_uniformSample rules.
Relational/Basic: Relational triple (RelTriple) with coupling rules for oracle queries — identity coupling, bijection/rnd rule, relTriple_bind, relTriple_refl, and bridges to evalDist/probOutput.
Relational/SimulateQ: Stateful relational coupling through simulateQ by induction on OracleComp, and the fundamental lemma of game playing (tvDist_simulateQ_le_probEvent_bad).
Relational/Quantitative: Full eRHL (ℝ≥0∞-valued relational Hoare logic) with pRHL and apRHL as special cases.
Notation: GameEquiv, AdvBound, bridge lemmas from RelTriple to game equivalence.
Fork: Forking lemma bridge to the program logic.

TV Distance & Probability (`VCVio/EvalDist/TVDist.lean`)

SPMF.tvDist, monadic tvDist with triangle inequality, map/bind monotonicity.
tvDist_le_probEvent_of_probOutput_eq_of_not — "identical until bad" TV bound.
abs_probOutput_toReal_sub_le_tvDist — Bool advantage ≤ TV distance.

Supporting Library

OptimalCoupling (ToMathlib/): Existence of optimal couplings for PMFs.
SampleableType: probOutput_bind_uniformBool (uniform-Boolean mixture), probOutput_map_bijective_uniformSample.
SubSpec: monadLift_eq_self simp lemma.
OracleComp/EvalDist: evalDist_simulateQ_run_eq_of_impl_evalDist_eq.
SigmaAlg → SigmaProtocol: Rename + game_rule simp set.

Fiat-Shamir (`VCVio/CryptoFoundations/FiatShamir.lean`)

Completeness proof (perfectlyCorrect) — 1 sorry remaining (simp regression from new @[simp] monadLift_eq_self).
EUF-CMA security theorem stated.

ElGamal IND-CPA (`Examples/HHS_Elgamal.lean`)

Main theorem: ElGamal_IND_CPA_le_q_mul_ddh — IND-CPA advantage ≤ q × DDH advantage.
Proven: random-mask bijection, all-random hybrid equivalence, all-random hybrid has probability 1/2, per-hop DDH reduction wiring.

Schnorr (`Examples/HHS_Schnorr.lean`)

New file with Schnorr signature security proof.

Sorry inventory (6 net new)

File	Count	Nature
`Relational/Quantitative.lean`	4	eRHL structural rules
`FiatShamir.lean`	1	simp regression in completeness proof
`Fork.lean`	1	Forking lemma bridge

Test plan

lake build passes (2764 jobs, zero errors)
No non-sorry warnings
Module layering DAG respected

…ative relational logic, and ElGamal wiring Add the complete program logic overhaul skeleton: - Unary/SimulateQ: wp rules for simulateQ, liftComp, stateful oracle impls - Relational/Quantitative: eRHL (ℝ≥0∞-valued) with pRHL and apRHL as special cases - Relational/SimulateQ: relational simulateQ coupling and identical-until-bad lemma - Notation: GameEquiv, AdvBound, game_wp/game_rel tactic macros - Basic: query coupling rules (identity + bijection/rnd) - RelationalAlgebra: two-sided StateT instance - SampleableType: bijective map + uniform bool guessing lemmas - HoareTriple: wp_ite rule - ElGamal: helper lemma statements for allRandomHalf and DDH step All proofs are either completed or sorry'd for parallel proof-filling. Made-with: Cursor

…l/SimulateQ Fill in proofs for relational coupling rules and simulateQ theorems: - Basic.lean: relTriple_query, relTriple_query_bij (bijection/"rnd" rule), plus relTriple_refl, relTriple_post_mono, relTriple_bind, and evalDist/probOutput equivalence bridges - SimulateQ.lean: relTriple_simulateQ_run (stateful oracle coupling by induction on OracleComp), relTriple_simulateQ_run' (output-only projection), and helper relTriple_map Made-with: Cursor

Unary/SimulateQ: all sorry's resolved — wp_simulateQ_eq, wp_liftComp, wp_simulateQ_run'_eq now fully proven. Relational/SimulateQ: fix "identical until bad" theorem signature — add required monotonicity hypotheses (h_mono₁, h_mono₂) without which the theorem is false. All helper lemmas fully proven; one sorry remains in the final tvDist bound (ENNReal algebra). Made-with: Cursor

Resolve three sorry's in the IND-CPA game-hopping proof: - randomMaskedCipher_dist_indep: left-multiplication bijection argument - IND_CPA_hybridOracle_allRandom_eqDist: relational coupling via evalDist equality - IND_CPA_allRandomHalf: uniform bit guessing reduces to probOutput_decide_eq_uniformBool_half Also add helper lemmas (evalDist_simulateQ_run_eq_of_impl_evalDist_eq, hybridChallengeOracle_allRandom_evalDist_eq) used in the coupling proof. Made-with: Cursor

github-actions · 2026-03-04T23:09:35Z

🤖 AI-Generated PR Summary

Files Changed:

Examples/HHS_Elgamal.lean
ToMathlib/Control/Monad/RelationalAlgebra.lean
VCVio.lean
VCVio/OracleComp/Constructions/SampleableType.lean
VCVio/ProgramLogic/Notation.lean
VCVio/ProgramLogic/Relational/Basic.lean
VCVio/ProgramLogic/Relational/Quantitative.lean
VCVio/ProgramLogic/Relational/SimulateQ.lean
VCVio/ProgramLogic/Unary/HoareTriple.lean
VCVio/ProgramLogic/Unary/SimulateQ.lean

Overview of Changes:
This diff significantly enhances the formal verification framework for cryptographic proofs by introducing a quantitative relational program logic and applying it to the IND-CPA security proof of ElGamal.

Here is a summary of the key changes:

New Quantitative Program Logic Framework (eRHL):
- A powerful quantitative relational Hoare logic (eRHL) is introduced. This framework allows reasoning not only about program equivalence but also about the statistical distance between program distributions, which is fundamental for computational security proofs.
- This includes core definitions for quantitative weakest preconditions (eRelWP) and rules for program composition (eRelTriple_bind).
High-Level Abstractions for Game-Hopping:
- The "identical until bad" lemma (tvDist_simulateQ_le_probEvent_bad) is formalized. This is a cornerstone of game-hopping proofs, providing a way to bound the difference between two games by the probability of a "bad" event.
- New rules (relTriple_simulateQ_run) are added to reason about the relationship between programs that simulate oracle queries differently.
Application to ElGamal Security Proof:
- The new logic is used to complete a key step in the IND-CPA security proof for ElGamal.
- It formally proves that in the "all-random hybrid" game, the adversary's view is statistically independent of the secret challenge bit. This directly implies that the adversary's advantage in this game is zero (success probability is exactly 1/2).
Improved Ergonomics and Helper Lemmas:
- A new file (Notation.lean) introduces more readable, user-facing notation and tactics to simplify writing proofs.
- Reusable probability lemmas, such as one for proving a game has a 1/2 success probability (probOutput_decide_eq_uniformBool_half), are added to streamline common proof patterns.

New 'sorry's: 11

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 8b32f36d81

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

chatgpt-codex-connector · 2026-03-04T23:13:59Z

VCVio/ProgramLogic/Notation.lean

+/-- `game_wp` decomposes unary WP goals by repeatedly applying WP rules. -/
+macro "game_wp" : tactic =>
+  `(tactic| (
+    simp only [game_rule]


Replace undefined game_rule references in game tactics

game_wp/game_rel both call simp with game_rule, but there is no game_rule lemma anywhere in the repository (a repo-wide rg "\bgame_rule\b" only finds these macro lines). As a result, the macros elaborate but fail when invoked with an unknown-constant error, so the new user-facing game-hopping tactics are not actually usable.

Useful? React with 👍 / 👎.

…d program logic tactics Rename `SigmaAlg` → `SigmaProtocol` with security property definitions (completeness, special soundness, HVZK). Add `game_rule` simp attribute, extend `game_wp`/`game_rel`/`coupling`/`game_hop` tactics, and wire up Schnorr sigma protocol and Fiat-Shamir examples. Made-with: Cursor

…l equivalence Fill the three Part A sorry's in HHS_Elgamal.lean: - hybridChallengeOracle_allRandom_evalDist_eq: the challenge oracle produces equal distributions for b=true vs b=false when realUntil=0, via StateT/liftM unfolding and randomMaskedCipher_dist_indep. - evalDist_monadLift_self: identity lift simplification using simulateQ_id'. - Minor SubSpec.lean comment fix. Made-with: Cursor

…ij, tvDist_simulateQ bound Fill sorry's in three program logic files: - wp_uniformSample via μ_bind_eq_tsum decomposition - relTriple_uniformSample_bij via relWP coupling with bijection - tvDist_simulateQ_le_probEvent_bad via fundamental lemma of game playing Made-with: Cursor

… and OptimalCoupling - Generalize IsQueryBound to arbitrary budget types; recover classical per-index bound as IsPerIndexQueryBound - Prove Schnorr sigma protocol completeness, special soundness, and HVZK - Fill eRelTriple_pure, relTriple'_bind, and backward direction of relTriple'_iff_couplingPost - Add OptimalCoupling.lean with compactness infrastructure for coupling space - Inline trueProbReal, weaken IND_CPA hybrid theorem hypotheses - Remove unused DecidableEq constraints from DDH/HHS definitions Made-with: Cursor

github-actions · 2026-03-06T20:52:39Z

🤖 Gemini PR Summary

Program Logic & Mathematical Foundations

Quantitative Relational Hoare Logic (eRHL): Implements eRelWP and eRelTriple, an $\mathbb{R}_{\ge 0 \infty}$-valued relational logic for OracleComp that generalizes probabilistic (pRHL) and approximate (apRHL) variants.
Oracle Simulation Rules: Establishes weakest-precondition (WP) rules for simulateQ (wp_simulateQ_eq, wp_simulateQ_run'_eq), enabling formal reasoning across stateful oracle boundaries.
Relational Coupling: Defines RelTriple with rules for oracle queries, including identity coupling, bijection/randomization rules, and the fundamental lemma of game playing (tvDist_simulateQ_le_probEvent_bad).
Total Variation (TV) Distance: Adds a TV distance infrastructure for SPMF featuring triangle inequality, bind/map monotonicity, and the "identical until bad" lemma (tvDist_le_probEvent_of_probOutput_eq_of_not).
Optimal Couplings: Provides the topological foundations for the existence of optimal couplings between PMFs on finite types in ToMathlib/.
Forking Lemma: Adds a bridge between the forking lemma and the program logic framework in Fork.lean.

Cryptographic Applications

ElGamal IND-CPA: Formalizes the security reduction showing ElGamal IND-CPA advantage is bounded by $q \times \text{Adv}^{\text{DDH}}$. Includes random-mask bijections and hybrid arguments.
Schnorr Protocol: Implements the Schnorr $\Sigma$-protocol for additive torsors, proving completeness, special soundness, and honest-verifier zero-knowledge (HVZK).
Fiat-Shamir Transform: Defines the transform's completeness and EUF-CMA security bounds.
$\Sigma$-Protocols: Refactors the SigmaAlg structure into SigmaProtocol with standardized definitions for cryptographic primitives.

Infrastructure & Automation

Tactics & Automation: Introduces the @[game_rule] attribute and specialized tactics (game_hop, game_wp) to automate relational and unary weakest-precondition goals.
Query Complexity: Refactors adversaries to use IsPerIndexQueryBound for granular per-oracle query enforcement.
Generalization: Removes DecidableEq constraints in DDH and TV distance lemmas to support classical reasoning.
Monadic Identities: Adds monadLift_eq_self as a simplification lemma for OracleComp lifts.

Critical Technical Note: Sorry Inventory (6 net new)

File	Count	Nature
`VCVio/ProgramLogic/Relational/Quantitative.lean`	4	Structural eRHL rules (sequential bind and statistical distance identification).
`VCVio/ProgramLogic/Fork.lean`	1	Probabilistic forking lemma bridge.
`VCVio/CryptoFoundations/FiatShamir.lean`	1	Regression in completeness proof due to `monadLift_eq_self` simplification behavior.

Statistics

Metric	Count
📝 Files Changed	33
✅ Lines Added	4029
❌ Lines Removed	195

Lean Declarations

✏️ **Removed:** 4 declaration(s)

lemma isQueryBound_bind {oa : OracleComp spec α} {ob : α → OracleComp spec β} in VCVio/OracleComp/QueryTracking/QueryBound.lean
theorem wp_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) in VCVio/ProgramLogic/Unary/HoareTriple.lean
lemma IsQueryBound.mono {oa : OracleComp spec α} {qb qb' : ι → ℕ} in VCVio/OracleComp/QueryTracking/QueryBound.lean
theorem wp_query (t : spec.Domain) (post : spec.Range t → ℝ≥0∞) : in VCVio/ProgramLogic/Unary/HoareTriple.lean

✏️ **Added:** 81 declaration(s)

theorem wp_simulateQ_run'_eq {σ : Type} in VCVio/ProgramLogic/Unary/SimulateQ.lean
abbrev IsPerIndexQueryBound (oa : OracleComp spec α) (qb : ι → ℕ) : Prop in VCVio/OracleComp/QueryTracking/QueryBound.lean
def couplings_set (p : SubPMF α) (q : SubPMF β) : Set (Option (α × β) → ℝ) in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
lemma probOutput_mul_left_uniform (m x : P) : in Examples/HHS_Elgamal.lean
theorem wp_liftComp {ι' : Type*} {superSpec : OracleSpec ι'} in VCVio/ProgramLogic/Unary/SimulateQ.lean
theorem eRelTriple_conseq {pre pre' : ℝ≥0∞} in VCVio/ProgramLogic/Relational/Quantitative.lean
def stepDDH_randBranchCore in Examples/HHS_Elgamal.lean
def PerfectlyComplete (σ : SigmaProtocol S W PC SC Ω P p) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean
lemma abs_probOutput_toReal_sub_le_tvDist in VCVio/EvalDist/TVDist.lean
lemma isCompact_couplings_set (p : SubPMF α) (q : SubPMF β) : in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
lemma probOutput_bind_mul_left_uniform {β : Type} (m : P) (f : P → ProbComp β) (z : β) : in Examples/HHS_Elgamal.lean
lemma isPerIndexQueryBound_query_iff (t : ι) (qb : ι → ℕ) : in VCVio/OracleComp/QueryTracking/QueryBound.lean
lemma OracleComp.ProgramLogic.Relational.relTriple_uniformSample_bij in VCVio/ProgramLogic/Relational/Basic.lean
def AdvBound (game : OracleComp spec₁ Bool) (ε : ℝ) : Prop in VCVio/ProgramLogic/Notation.lean
theorem schnorrSigma_speciallySound : in Examples/HHS_Schnorr.lean
theorem spmf_tvDist_eq_one_sub_eRelWP_eqRel in VCVio/ProgramLogic/Relational/Quantitative.lean
lemma relTriple'_bind in VCVio/ProgramLogic/Relational/Quantitative.lean
lemma isPerIndexQueryBound_query_bind_iff (t : ι) (mx : spec t → OracleComp spec α) in VCVio/OracleComp/QueryTracking/QueryBound.lean
lemma isClosed_couplings_set (p : SubPMF α) (q : SubPMF β) : in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
lemma map_fst_eval (c : SubPMF (α × β)) (a : α) : in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
lemma probEvent_subpmf_eq_spmf (p : SPMF α) (q : α → Prop) : in VCVio/EvalDist/Instances/OptionT.lean
lemma finSupport_nonempty [HasEvalFinset m] [DecidableEq α] (mx : m α) : in VCVio/EvalDist/Defs/Basic.lean
lemma probOutput_map_bijective_uniformSample [Fintype α] in VCVio/OracleComp/Constructions/SampleableType.lean
lemma IND_CPA_hybridOracle_allRandom_eqDist in Examples/HHS_Elgamal.lean
lemma probOutput_congr_evalDist {oa ob : OracleComp spec α} in VCVio/ProgramLogic/Unary/HoareTriple.lean
def stepDDH_realBranchGame in Examples/HHS_Elgamal.lean
lemma μ_congr_evalDist {oa ob : OracleComp spec ℝ≥0∞} in VCVio/ProgramLogic/Unary/HoareTriple.lean
theorem wp_simulateQ_eq in VCVio/ProgramLogic/Unary/SimulateQ.lean
theorem schnorrSigma_hvzk : in Examples/HHS_Schnorr.lean
lemma SubPMF.exists_max_coupling {p : SubPMF α} {q : SubPMF β} in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
def eRelTriple (pre : ℝ≥0∞) (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) in VCVio/ProgramLogic/Relational/Quantitative.lean
theorem euf_cma_bound in VCVio/CryptoFoundations/FiatShamir.lean
theorem relTriple'_iff_relTriple in VCVio/ProgramLogic/Relational/Quantitative.lean
def GameEquiv (g₁ g₂ : OracleComp spec₁ α) : Prop in VCVio/ProgramLogic/Notation.lean
theorem relTriple'_iff_couplingPost in VCVio/ProgramLogic/Relational/Quantitative.lean
def schnorrSigma : SigmaProtocol (P × P) G P G Bool G in Examples/HHS_Schnorr.lean
theorem eRelTriple_bind in VCVio/ProgramLogic/Relational/Quantitative.lean
lemma ddh_decomp_two_games_toReal (real rand : ProbComp Bool) : in Examples/HHS_Elgamal.lean
def RelTriple' (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) in VCVio/ProgramLogic/Relational/Quantitative.lean
theorem relTriple_simulateQ_run in VCVio/ProgramLogic/Relational/SimulateQ.lean
lemma relTriple_query (t : spec₁.Domain) : in VCVio/ProgramLogic/Relational/Basic.lean
theorem tvDist_eq_one_sub_eRelWP_eqRel in VCVio/ProgramLogic/Relational/Quantitative.lean
lemma monadLift_eq_self {α} (mx : OracleComp spec α) : in VCVio/OracleComp/Coercions/SubSpec.lean
lemma randomMaskedCipher_dist_indep (pk : P × P) (m₁ m₂ : P) : in Examples/HHS_Elgamal.lean
theorem IND_CPA_HybridGame_q_eq_game in Examples/HHS_Elgamal.lean
lemma isPerIndexQueryBound_pure (x : α) (qb : ι → ℕ) : in VCVio/OracleComp/QueryTracking/QueryBound.lean
lemma isPerIndexQueryBound_map_iff (oa : OracleComp spec α) (f : α → β) (qb : ι → ℕ) : in VCVio/OracleComp/QueryTracking/QueryBound.lean
def ApproxRelTriple (ε : ℝ≥0∞) (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) in VCVio/ProgramLogic/Relational/Quantitative.lean
def IND_CPA_adversary.MakesAtMostQueries {encAlg : AsymmEncAlg ProbComp M PK SK C} in VCVio/CryptoFoundations/AsymmEncAlg.lean
theorem relTriple'_eq_approxRelTriple_zero in VCVio/ProgramLogic/Relational/Quantitative.lean
theorem triple_fork (post : α × α → ℝ≥0∞) : in VCVio/ProgramLogic/Fork.lean
lemma isPerIndexQueryBound_bind {oa : OracleComp spec α} {ob : α → OracleComp spec β} in VCVio/OracleComp/QueryTracking/QueryBound.lean
lemma μ_cross_congr_evalDist {ι' : Type*} {spec' : OracleSpec ι'} in VCVio/ProgramLogic/Unary/HoareTriple.lean
lemma relTriple_query_bij (t : spec₁.Domain) in VCVio/ProgramLogic/Relational/Basic.lean
lemma probOutput_subpmf_eq_spmf (p : SPMF α) (x : α) : in VCVio/EvalDist/Instances/OptionT.lean
theorem GameEquiv.of_relTriple' in VCVio/ProgramLogic/Notation.lean
lemma tvDist_le_probEvent_of_probOutput_eq_of_not in VCVio/EvalDist/TVDist.lean
theorem tvDist_simulateQ_le_probEvent_bad in VCVio/ProgramLogic/Relational/SimulateQ.lean
lemma relTriple_map {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} in VCVio/ProgramLogic/Relational/Basic.lean
def stepDDH_randBranchGame in Examples/HHS_Elgamal.lean
theorem perfectlyCorrect (hc : σ.PerfectlyComplete) : in VCVio/CryptoFoundations/FiatShamir.lean
def HVZK (σ : SigmaProtocol S W PC SC Ω P p) in VCVio/CryptoFoundations/SigmaProtocol.lean
theorem AdvBound.of_tvDist in VCVio/ProgramLogic/Notation.lean
theorem eRelTriple_pure (a : α) (b : β) (post : α → β → ℝ≥0∞) : in VCVio/ProgramLogic/Relational/Quantitative.lean
lemma probOutput_decide_eq_uniformBool_half in VCVio/OracleComp/Constructions/SampleableType.lean
lemma probOutput_bind_uniformBool {α : Type} in VCVio/OracleComp/Constructions/SampleableType.lean
theorem relTriple_simulateQ_run' in VCVio/ProgramLogic/Relational/SimulateQ.lean
theorem schnorrSigma_complete : in Examples/HHS_Schnorr.lean
lemma run_liftM [Monad m] (x : m α) (s : σ) : in ToMathlib/Control/StateT.lean
lemma IsPerIndexQueryBound.mono {oa : OracleComp spec α} {qb qb' : ι → ℕ} in VCVio/OracleComp/QueryTracking/QueryBound.lean
theorem GameEquiv.of_approxRelTriple_zero in VCVio/ProgramLogic/Notation.lean
def SpeciallySound (σ : SigmaProtocol S W PC SC Ω P p) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean
lemma mem_couplings_set_of_isCoupling {p : SubPMF α} {q : SubPMF β} (c : SubPMF (α × β)) in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
theorem gameEquiv_of_relTriple'_eqRel in VCVio/ProgramLogic/Relational/Quantitative.lean
lemma wp_congr_evalDist {oa ob : OracleComp spec α} in VCVio/ProgramLogic/Unary/HoareTriple.lean
lemma map_snd_eval (c : SubPMF (α × β)) (b : β) : in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
def stepDDH_realBranchCore in Examples/HHS_Elgamal.lean
lemma isBounded_couplings_set (p : SubPMF α) (q : SubPMF β) : in ToMathlib/ProbabilityTheory/OptimalCoupling.lean
def SpeciallySoundAt (σ : SigmaProtocol S W PC SC Ω P p) (x : S) : Prop in VCVio/CryptoFoundations/SigmaProtocol.lean
lemma indicator_objective_eq_probEvent (mx : m (α × β)) (R : α → β → Prop) : in VCVio/EvalDist/Defs/Basic.lean
lemma evalDist_simulateQ_run_eq_of_impl_evalDist_eq in VCVio/OracleComp/EvalDist.lean

✏️ **Affected:** 15 declaration(s) (line number changed)

def IsQueryBound (oa : OracleComp spec α) (budget : B) in VCVio/OracleComp/QueryTracking/QueryBound.lean moved from L33 to L42
def parallelTesting_experiment in VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean moved from L56 to L56
theorem ElGamal_IND_CPA_bound_toReal in Examples/HHS_Elgamal.lean moved from L252 to L2018
lemma tvDist_map_le [LawfulMonad m] {β : Type u} (f : α → β) (mx my : m α) : in VCVio/EvalDist/TVDist.lean moved from L84 to L87
def IND_CPA_stepDDHReduction in Examples/HHS_Elgamal.lean moved from L213 to L406
theorem ElGamal_IND_CPA_le_q_mul_ddh in Examples/HHS_Elgamal.lean moved from L292 to L2066
lemma IND_CPA_stepDDH_hopBound in Examples/HHS_Elgamal.lean moved from L235 to L1654
lemma tvDist_map_le (f : α' → β) (p q : PMF α') : in ToMathlib/Probability/ProbabilityMassFunction/TotalVariation.lean moved from L141 to L142
abbrev ddhExp (adversary : DDHAdversary V P) : ProbComp Bool in VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean moved from L49 to L49
lemma etvDist_map_le (f : α' → β) (p q : PMF α') : in ToMathlib/Probability/ProbabilityMassFunction/TotalVariation.lean moved from L126 to L126
lemma isQueryBound_query_bind_iff (t : ι) (mx : spec t → OracleComp spec α) in VCVio/OracleComp/QueryTracking/QueryBound.lean moved from L44 to L55
lemma isQueryBound_query_iff (t : ι) (b : B) in VCVio/OracleComp/QueryTracking/QueryBound.lean moved from L50 to L62
def FiatShamir (sigmaAlg : SigmaProtocol X W PC SC Ω P p) in VCVio/CryptoFoundations/FiatShamir.lean moved from L35 to L35
lemma isQueryBound_pure (x : α) (b : B) in VCVio/OracleComp/QueryTracking/QueryBound.lean moved from L41 to L51
lemma isQueryBound_map_iff (oa : OracleComp spec α) (f : α → β) (b : B) in VCVio/OracleComp/QueryTracking/QueryBound.lean moved from L118 to L82

sorry Tracking

✅ **Removed:** 2 `sorry`(s)

lemma IND_CPA_stepDDH_hopBound in Examples/HHS_Elgamal.lean (L242)
theorem IND_CPA_allRandomHalf in Examples/HHS_Elgamal.lean (L175)

❌ **Added:** 6 `sorry`(s)

theorem perfectlyCorrect (hc : σ.PerfectlyComplete) : in VCVio/CryptoFoundations/FiatShamir.lean (L141)
theorem spmf_tvDist_eq_one_sub_eRelWP_eqRel in VCVio/ProgramLogic/Relational/Quantitative.lean (L428)
theorem euf_cma_bound in VCVio/CryptoFoundations/FiatShamir.lean (L174)
theorem euf_cma_bound in VCVio/CryptoFoundations/FiatShamir.lean (L175)
theorem eRelTriple_bind in VCVio/ProgramLogic/Relational/Quantitative.lean (L413)
theorem triple_fork (post : α × α → ℝ≥0∞) : in VCVio/ProgramLogic/Fork.lean (L40)

📄 **Per-File Summaries**

Examples.lean: The update integrates the HHS Schnorr protocol example into the project by adding an import for Examples.HHS_Schnorr. This ensures that the formalizations and proofs related to this protocol are included in the top-level examples list.
Examples/HHS_Elgamal.lean: This change completes the formal proof of IND-CPA security for ElGamal over Hard Homogeneous Spaces by replacing previous sorry placeholders with rigorous proofs. It introduces several new lemmas concerning probability distributions and decisional Diffie-Hellman (DDH) reductions to establish the per-hop bounds in the hybrid argument. The final main theorem now provides a fully verified bound on the IND-CPA advantage based on the adversary's query budget and the DDH advantage.
Examples/HHS_Schnorr.lean: This file defines a Schnorr-like Σ-protocol for additive torsors (Hard Homogeneous Spaces) and formalizes its core security properties. It introduces the schnorrSigma protocol definition along with proofs for its perfect completeness, special soundness, and honest-verifier zero-knowledge (HVZK) properties. No sorry or admit placeholders are used.
ToMathlib.lean: This change updates the ToMathlib.lean aggregation file to include a new module for optimal couplings in probability theory. No new definitions, theorems, or sorry placeholders are introduced directly in this file.
ToMathlib/Control/Monad/RelationalAlgebra.lean: This change introduces a new MAlgRelOrdered instance, instStateTBoth, which enables relational reasoning between two StateT monads carrying distinct state types. It provides the definition and complete proofs for the relational weakest precondition (rwp) and its properties without any sorry placeholders.
ToMathlib/Control/StateT.lean: This update introduces the run_liftM simp lemma, which characterizes the execution of a lifted monadic action within the StateT monad transformer. No sorry or admit placeholders are introduced.
ToMathlib/Probability/ProbabilityMassFunction/TotalVariation.lean: These changes generalize the etvDist_map_le and tvDist_map_le lemmas by removing the [DecidableEq β] constraint and instead using the classical tactic in their proofs. The modifications allow these theorems for total variation distance to apply to functions targeting types without decidable equality.
ToMathlib/ProbabilityTheory/OptimalCoupling.lean: This file establishes the compactness of the space of couplings between two SubPMFs on finite types by embedding them into a real-valued function space. It provides the topological foundations and technical lemmas necessary to prove SubPMF.exists_max_coupling, which shows that linear objective functions (such as expected values) attain their maximum over the set of possible couplings. The file contains no sorry placeholders.
VCVio.lean: This change updates the library's top-level imports to include new program logic modules for forking, specialized notation, and quantitative reasoning in relational and unary contexts. It also renames the foundation module for Sigma protocols from SigmaAlg to SigmaProtocol.
VCVio/CryptoFoundations/AsymmEncAlg.lean: This PR introduces the IND_CPA_adversary.MakesAtMostQueries definition to formally bound the number of challenge oracle queries an adversary can perform. Additionally, it refactors the hybrid argument lemmas by removing the trueProbReal abbreviation and weakening theorem hypotheses to require only equality of probabilities rather than equality of the underlying games. No sorry or admit placeholders were added.
VCVio/CryptoFoundations/FiatShamir.lean: This update renames the underlying primitive to SigmaProtocol and begins formalizing the properties of the Fiat-Shamir transform. It introduces new theorems for the scheme's completeness (perfectlyCorrect) and EUF-CMA security (euf_cma_bound), though both currently contain sorry placeholders.
VCVio/CryptoFoundations/HardnessAssumptions/DiffieHellman.lean: This change generalizes the Decisional Diffie-Hellman (DDH) experiment and advantage definitions by removing unnecessary DecidableEq V type class constraints. It modifies existing definitions without introducing new theorems or sorry placeholders.
VCVio/CryptoFoundations/HardnessAssumptions/HardHomogeneousSpace.lean: The changes remove the unnecessary DecidableEq G typeclass constraint from the parallelTesting_experiment and parallelTestingAdvantage definitions. This modification simplifies the requirements for defining the parallel testing experiment in the context of hard homogeneous spaces.
VCVio/CryptoFoundations/SecExp.lean: This change modifies the SecAdv structure to require an IsPerIndexQueryBound property instead of IsQueryBound. This updates the definition of security adversaries to track and enforce query complexity bounds specifically on a per-oracle index basis.
VCVio/CryptoFoundations/SigmaAlg.lean: This change deletes the SigmaAlg.lean file, removing the SigmaAlg structure definition for Sigma protocols. The structure had previously defined the core components of these protocols, including commitment generation, response functions, and verification logic.
VCVio/CryptoFoundations/SigmaProtocol.lean: This file introduces a new SigmaProtocol structure to formalize cryptographic Σ-protocols, including fields for commitment, response, verification, simulation, and extraction. It also provides definitions for standard security properties: perfect completeness, special soundness, and honest-verifier zero-knowledge (HVZK). No sorry placeholders are used in the new definitions.
VCVio/EvalDist/Defs/Basic.lean: This PR introduces two new lemmas to the library: finSupport_nonempty, which proves that the finite support of a distribution is always non-empty, and indicator_objective_eq_probEvent, which equates a sum involving an indicator function to the probability of the corresponding event. No sorry or admit placeholders were added.
VCVio/EvalDist/Instances/OptionT.lean: This change introduces theorems probOutput_subpmf_eq_spmf and probEvent_subpmf_eq_spmf to bridge the SubPMF and SPMF representations of probability distributions. These lemmas establish that probOutput and probEvent are equivalent across both views, which are both defined as OptionT PMF but carry different typeclass instances.
VCVio/EvalDist/Monad/Basic.lean: This change adds the game_rule attribute to several fundamental lemmas relating evaluation distributions and probability outputs for pure and bind operations. These updates integrate these core monadic properties into the library's automated reasoning framework for game-based proofs without introducing new theorems or sorry placeholders.
VCVio/EvalDist/TVDist.lean: This change introduces two new theorems, tvDist_le_probEvent_of_probOutput_eq_of_not and abs_probOutput_toReal_sub_le_tvDist, for bounding the total variation distance between monadic computations, particularly for those that never fail. Additionally, it removes unnecessary DecidableEq constraints from existing mapping lemmas and includes necessary imports for reasoning about computations that succeed with probability one. No sorry or admit placeholders were added.
VCVio/OracleComp/Coercions/SubSpec.lean: This change introduces a new simplification lemma, monadLift_eq_self, which proves that lifting an OracleComp to its own specification is an identity operation. No sorry or admit placeholders are added.
VCVio/OracleComp/Constructions/SampleableType.lean: This file introduces several new lemmas for reasoning about the output probabilities of uniform distributions, particularly for the Bool type. Key additions include theorems for bijective mappings of uniform samples and a proof that guessing a bit independent of its underlying distribution results in a success probability of exactly 1/2.
VCVio/OracleComp/EvalDist.lean: This change introduces the lemma evalDist_simulateQ_run_eq_of_impl_evalDist_eq, which proves that two oracle simulations yield the same probability distribution if their underlying query implementations are distributionally equivalent. The new proof is completed without any sorry or admit placeholders.
VCVio/OracleComp/QueryTracking/QueryBound.lean: This Lean file generalizes the IsQueryBound predicate to support arbitrary budget types, query validity checks, and cost functions, while re-implementing the original per-index query tracking as IsPerIndexQueryBound. The change updates existing structural lemmas and the PolyQueries definition to align with this new framework without introducing any sorry placeholders.
VCVio/OracleComp/SimSemantics/SimulateQ.lean: This change imports VCVio.Prelude and adds the game_rule attribute to the existing lemmas simulateQ_pure, simulateQ_bind, and simulateQ_query. These modifications integrate simulation semantics for queries with specialized tactics for reasoning about cryptographic games without introducing new theorems or sorry placeholders.
VCVio/Prelude.lean: This change introduces the game_rule simplification attribute, which is intended to categorize and collect lemmas for game-hopping proofs involving probability distributions and weakest preconditions. No new theorems, definitions, or sorry placeholders were added.
VCVio/ProgramLogic/Fork.lean: This file introduces the triple_fork theorem, which expresses the probabilistic forking lemma as a quantitative Hoare triple within the program logic framework. The theorem's proof currently contains a sorry placeholder.
VCVio/ProgramLogic/Notation.lean: This file introduces a convenience layer for program logic by defining predicates for game equivalence (GameEquiv) and advantage bounds (AdvBound), along with several bridge theorems. It also provides a suite of tactics, including game_hop and game_wp, to automate the decomposition of unary and relational goals in cryptographic game-hopping proofs. No sorry or admit placeholders are introduced.
VCVio/ProgramLogic/Relational/Basic.lean: This change introduces several new relational coupling lemmas for probabilistic relational Hoare logic (pRHL) in OracleComp. These include identity and bijection coupling rules for oracle queries, a rule for mapped computations, and a coupling rule for uniform sampling from SampleableType via bijections. The file adds these new theorems without using any sorry or admit placeholders.
VCVio/ProgramLogic/Relational/Quantitative.lean: This file introduces quantitative relational program logic (eRHL) for OracleComp by defining ℝ≥0∞-valued weakest preconditions (eRelWP) and triples (eRelTriple) that generalize both exact and approximate relational logic. It establishes bridge theorems to existing pRHL/apRHL definitions and provides fundamental logical rules, though the sequential bind rule and statistical distance identification currently contain sorry placeholders.
VCVio/ProgramLogic/Relational/SimulateQ.lean: This new file establishes relational coupling theorems for stateful oracle simulations (simulateQ) and proves the "identical until bad" lemma for bounding total variation distance. It introduces several new theorems and supporting lemmas for game-hopping proofs, with no sorry placeholders.
VCVio/ProgramLogic/Unary/HoareTriple.lean: This update extends the quantitative weakest precondition (wp) framework for OracleComp by adding congruence lemmas for wp under distributional equality and a new rule for uniform sampling from SampleableType. It also introduces a wp_ite theorem for conditional logic and annotates several core rules with the @[game_rule] attribute to facilitate automated reasoning. No sorry or admit placeholders are introduced.
VCVio/ProgramLogic/Unary/SimulateQ.lean: This new file introduces several theorems connecting quantitative weakest preconditions (wp) to oracle simulation semantics. These results, including wp_simulateQ_eq and wp_liftComp, establish that wp is preserved under distribution-preserving oracle implementations and subspec lifting; the file contains no sorry placeholders.

Last updated: 2026-03-07 02:34 UTC.

…ain) Define IND_CPA_allRealChallengeOracle / IND_CPA_queryImpl_allReal and the lemma chain (allReal_eq_hybrid_on_bounded, hybrid_q_probOutput_eq_allReal, allReal_evalDist_proj_eq_real, hybrid_q_run'_evalDist_eq_real) that proves IND_CPA_HybridGame_q_eq_game: hybrid game at q equals the real IND-CPA game when the adversary MakesAtMostQueries q. Land ElGamal_IND_CPA_le_q_mul_ddh with the locked-in statement using MakesAtMostQueries. Remove unused ddh_decomp_two_games, inline trueProbReal, tighten longFile limit. Four sorry's remain in the allReal simulation lemmas (term-matching issues, not logical gaps). Made-with: Cursor

Match upstream mathlib PR #35826 review feedback: remove [DecidableEq β] from type signatures where it is only needed in the proof, and use `classical` instead. Made-with: Cursor

Complete the final allReal and projection lemmas so the HHS ElGamal IND-CPA proof closes without remaining sorries. Made-with: Cursor

Establish the finite-support projection and coupling reconstruction lemmas so the compactness argument yields an actual maximizing coupling. Made-with: Cursor

Prove the remaining Wave 1 eRHL bridge lemmas so the quantitative relational logic file builds cleanly except for the intended Wave 2 placeholders. Made-with: Cursor

…mpleteness Add total variation distance infrastructure (SPMF.tvDist, monadic tvDist), probability lemmas (probOutput_bind_uniformBool, monadLift_eq_self, evalDist_simulateQ_run_eq), and extend program logic with quantitative relational rules. Begin Fiat-Shamir completeness proof and fix ElGamal linter warnings. Made-with: Cursor

quangvdao added 4 commits March 4, 2026 13:40

chatgpt-codex-connector bot reviewed Mar 4, 2026

View reviewed changes

quangvdao added 4 commits March 4, 2026 21:56

quangvdao added 6 commits March 7, 2026 05:04

chore: remove unused [DecidableEq β] from tvDist_map_le lemmas

6eb021e

Match upstream mathlib PR #35826 review feedback: remove [DecidableEq β] from type signatures where it is only needed in the proof, and use `classical` instead. Made-with: Cursor

feat(ElGamal): finish hybrid-to-real IND-CPA bridge

33e13c4

Complete the final allReal and projection lemmas so the HHS ElGamal IND-CPA proof closes without remaining sorries. Made-with: Cursor

feat(ToMathlib): prove optimal coupling existence

b665e6a

Establish the finite-support projection and coupling reconstruction lemmas so the compactness argument yields an actual maximizing coupling. Made-with: Cursor

feat(ProgramLogic): finish quantitative bridge lemmas

f428692

Prove the remaining Wave 1 eRHL bridge lemmas so the quantitative relational logic file builds cleanly except for the intended Wave 2 placeholders. Made-with: Cursor

quangvdao changed the title ~~feat(ProgramLogic): program logic overhaul — eRHL, simulateQ rules, and ElGamal all-random proof~~ feat(ProgramLogic): eRHL program logic, TV distance, Fiat-Shamir, and ElGamal IND-CPA Mar 7, 2026

Merge branch 'master' into quang/more-program-logic

ab84f03

quangvdao merged commit f658ff1 into master Mar 7, 2026
4 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(ProgramLogic): eRHL program logic, TV distance, Fiat-Shamir, and ElGamal IND-CPA#116

feat(ProgramLogic): eRHL program logic, TV distance, Fiat-Shamir, and ElGamal IND-CPA#116
quangvdao merged 15 commits intomasterfrom
quang/more-program-logic

quangvdao commented Mar 4, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 4, 2026

Uh oh!

chatgpt-codex-connector bot left a comment

Uh oh!

chatgpt-codex-connector bot Mar 4, 2026

Uh oh!

github-actions bot commented Mar 6, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

quangvdao commented Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Program Logic (VCVio/ProgramLogic/)

TV Distance & Probability (VCVio/EvalDist/TVDist.lean)

Supporting Library

Fiat-Shamir (VCVio/CryptoFoundations/FiatShamir.lean)

ElGamal IND-CPA (Examples/HHS_Elgamal.lean)

Schnorr (Examples/HHS_Schnorr.lean)

Sorry inventory (6 net new)

Test plan

Uh oh!

github-actions bot commented Mar 4, 2026

🤖 AI-Generated PR Summary

Uh oh!

chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector bot Mar 4, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Mar 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Gemini PR Summary

Program Logic & Mathematical Foundations

Cryptographic Applications

Infrastructure & Automation

Critical Technical Note: Sorry Inventory (6 net new)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

quangvdao commented Mar 4, 2026 •

edited

Loading

Program Logic (`VCVio/ProgramLogic/`)

TV Distance & Probability (`VCVio/EvalDist/TVDist.lean`)

Fiat-Shamir (`VCVio/CryptoFoundations/FiatShamir.lean`)

ElGamal IND-CPA (`Examples/HHS_Elgamal.lean`)

Schnorr (`Examples/HHS_Schnorr.lean`)

github-actions bot commented Mar 6, 2026 •

edited

Loading